;;;============================================================
;;;
;;; Subject: Generator of simplicial complex from a 3d digital
;;;          image
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Beginning date: 24-12-10
;;; End date: 
;;;
;;;============================================================



(in-package "ACL2")

(defun list-0-1p (list)
  (if (endp list)
      (equal list nil)
    (if (endp (cdr list))
	(and (equal (cdr list) nil)
	     (or (equal (car list) 0)
		 (equal (car list) 1)))
      (and (or (equal (car list) 0)
	       (equal (car list) 1))
	   (list-0-1p (cdr list))))))

(defun list-of-lists-of-0-1p (list)
  (if (endp list)
      (equal list nil)
    (and (list-0-1p (car list))
	 (list-of-lists-of-0-1p (cdr list)))))


(defun 3d-imagep (3da)
  (if (endp 3da)
      (equal 3da nil)
    (and (list-of-lists-of-0-1p (car 3da))
	 (3d-imagep (cdr 3da)))))

(defun genera-facet-1 (i j k)
  (list (list i j k) 
	(list (1+ i) j k)
	(list (1+ i) j (1+ k))
	(list (1+ i) (1+ j) (1+ k))))

(defun genera-facet-2 (i j k)
  (list (list i j k) 
	(list (1+ i) j k)
	(list (1+ i) (1+ j) k)
	(list (1+ i) (1+ j) (1+ k))))

(defun genera-facet-3 (i j k)
  (list (list i j k) 
	(list i j (1+ k))
	(list (1+ i) j (1+ k))
	(list (1+ i) (1+ j) (1+ k))))

(defun genera-facet-4 (i j k)
  (list (list i j k) 
	(list i j (1+ k))
	(list i (1+ j) (1+ k))
	(list (1+ i) (1+ j) (1+ k))))

(defun genera-facet-5 (i j k)
  (list (list i j k) 
	(list i (1+ j) k)
	(list (1+ i) (1+ j) k)
	(list (1+ i) (1+ j) (1+ k))))

(defun genera-facet-6 (i j k)
  (list (list i j k) 
	(list i (1+ j) k)
	(list i (1+ j) (1+ k))
	(list (1+ i) (1+ j) (1+ k))))


(defun genera-facets-i-j-k (i j k)
  (list (genera-facet-1 i j k)
	(genera-facet-2 i j k)
	(genera-facet-3 i j k)
	(genera-facet-4 i j k)
	(genera-facet-5 i j k)
	(genera-facet-6 i j k)))

(defun genera-facets-line (list i j k)
  (if (endp list)
      nil
    (if (equal (car list) 1)
	(append (genera-facets-i-j-k i j k)
		(genera-facets-line (cdr list) (1+ i) j k))
      (genera-facets-line (cdr list) (1+ i) j k))))

(defun genera-facets-layer (list j k)
  (if (endp list)
      nil
    (append (genera-facets-line (car list) 0 j k)
	    (genera-facets-layer (cdr list) (1+ j) k))))

(defun genera-facets-3d-image-aux (list k)
  (if (endp list)
      nil
    (append (genera-facets-layer (car list) 0 k)
	    (genera-facets-3d-image-aux (cdr list) (1+ k)))))

(defun genera-facets-image-3d (3da)
  (genera-facets-3d-image-aux 3da 0))





;;;---------------------------------------------------------------------------
;;;
;;; Property: genera-facets-image generates a list of simplexes over (N,N,N)
;;;
;;;---------------------------------------------------------------------------

(defun l-ord (list1 list2)
  (cond ((and (endp list1) (endp list2)) nil)
	((endp list1) t)
	((endp list2) nil)
	((< (car list1) (car list2)) t)
	(t (l-ord (cdr list1) (cdr list2)))))
 

(defun nat-listp (list)
  (if (endp list)
      (equal list nil)
    (and (natp (car list))
	 (nat-listp (cdr list)))))
	

(defun simplex-p (list)
  (if (endp list)
      (equal list nil)
    (if (endp (cdr list))
	(and (equal (cdr list) nil) (nat-listp (car list)))
      (and (nat-listp (car list)) (nat-listp (cadr list))
	   (l-ord (car list) (cadr list))
	   (simplex-p (cdr list))))))


(defun  simplex-n-n-n-p (list)
  (and (equal (len list) 4)
       (simplex-p list)))



(defun list-of-simplexes-n-n-n-p (lol)
  (if (endp lol)
      (equal lol nil)
    (and (simplex-n-n-n-p (car lol))
	 (list-of-simplexes-n-n-n-p (cdr lol)))))


(defthm append-list-of-simplexes-n-n-n-p
  (implies (and (list-of-simplexes-n-n-n-p x)
		(list-of-simplexes-n-n-n-p y))
	   (list-of-simplexes-n-n-n-p (append x y))))


(defthm genera-facets-line-generates-list-of-simplexes-n-n-n-p
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k))
	   (list-of-simplexes-n-n-n-p (genera-facets-line x i j k))))

(defthm genera-facets-layer-generates-list-of-simplexes-n-n-n-p
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k))
	   (list-of-simplexes-n-n-n-p (genera-facets-layer x j k))))

(defthm genera-facets-3d-image-aux-generates-list-of-simplexes-n-n-n-p
  (implies (and (3d-imagep x)
		(natp k))
	   (list-of-simplexes-n-n-n-p (genera-facets-3d-image-aux x k))))


(defthm genera-facets-image-3d-generates-list-of-simplexes-n-n-n-p
  (implies (3d-imagep image)
	   (list-of-simplexes-n-n-n-p (genera-facets-image-3d image))))



;;;---------------------------------------------------------------------------
;;;
;;; Property: The number of elements obtained from 
;;; genera-facets-image-3d is equal to 6 times the number
;;; of ones of the array associated with the image
;;;
;;;---------------------------------------------------------------------------

(encapsulate 
 ()

(defun count-1-list (list)
  (if (endp list)
      0
    (if (equal (car list) 1)
	(1+ (count-1-list (cdr list)))
      (count-1-list (cdr list)))))


(defun count-1-lol (lol)
  (if (endp lol)
      0
    (+ (count-1-list (car lol))
       (count-1-lol (cdr lol)))))


(defun count-1-image-3d (3da)
  (if (endp 3da)
      0
    (+ (count-1-lol (car 3da))
       (count-1-image-3d (cdr 3da)))))
		    


(local (defthm facets=6*number-of-1-genera-facets-line
  (implies (list-0-1p list)
	   (equal (len (genera-facets-line list i j k))
		  (* 6 (count-1-list list))))))

(local (defthm len-append
  (implies (consp x)
	   (equal (+ (len x) (len y))
		  (len (append x y))))))


(local (defthm facets=6*number-of-1-genera-facets-layer
  (implies (list-of-lists-of-0-1p list)
	   (equal (len (genera-facets-layer list j k))
		  (* 6 (count-1-lol list))))
  :hints (("Subgoal *1/3''" :use
	   ((:instance len-append (x (genera-facets-line (CAR list) 0 j k))
		       (y (genera-facets-layer (cdr list) (+ 1 j) k)))
	    (:instance facets=6*number-of-1-genera-facets-line (list (car list))
		       (i 0)))))))


(local (defthm facets=6*number-of-1-aux
  (implies (3d-imagep image)
	   (equal (len (genera-facets-3d-image-aux image k))
		  (* 6 (count-1-image-3d image))))
  :hints (("Subgoal *1/3''" :use
	   ((:instance len-append (x (genera-facets-layer (car image) 0 k))
		       (y (genera-facets-3d-image-aux (cdr image) (1+ k))))
	    (:instance facets=6*number-of-1-genera-facets-layer (list (car image))
		       (j 0) ))))))


(defthm facets=6*number-of-1
  (implies (3d-imagep image)
	   (equal (len (genera-facets-image-3d image))
		  (* 6 (count-1-image-3d image)))))

)



;;;---------------------------------------------------------------------------
;;;
;;; Additional definitions for the proofs
;;;
;;;---------------------------------------------------------------------------

(defun genera-facet-1-simplex (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (genera-facet-1 i j k)))

(defun genera-facet-2-simplex (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (genera-facet-2 i j k)))

(defun genera-facet-3-simplex (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (genera-facet-3 i j k)))

(defun genera-facet-4-simplex (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (genera-facet-4 i j k)))

(defun genera-facet-5-simplex (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (genera-facet-5 i j k)))

(defun genera-facet-6-simplex (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (genera-facet-6 i j k)))


(defun member-type-1 (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (equal (genera-facet-1 i j k) simplex)))

(defun member-type-2 (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (equal (genera-facet-2 i j k) simplex)))

(defun member-type-3 (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (equal (genera-facet-3 i j k) simplex)))

(defun member-type-4 (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (equal (genera-facet-4 i j k) simplex)))

(defun member-type-5 (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (equal (genera-facet-5 i j k) simplex)))

(defun member-type-6 (simplex)
  (let ((i (nth 0 (car simplex)))
	(j (nth 1 (car simplex)))
	(k (nth 2 (car simplex))))
  (equal (genera-facet-6 i j k) simplex)))

;;;***************************************************************************
;;;
;;; Relations among the above functions
;;;
;;;***************************************************************************

(defthm genera-facet-1-simplex-member-type-1
  (member-type-1 (genera-facet-1-simplex simplex)))

(defthm genera-facet-2-simplex-member-type-2
  (member-type-2 (genera-facet-2-simplex simplex)))

(defthm genera-facet-3-simplex-member-type-3
  (member-type-3 (genera-facet-3-simplex simplex)))

(defthm genera-facet-4-simplex-member-type-4
  (member-type-4 (genera-facet-4-simplex simplex)))

(defthm genera-facet-5-simplex-member-type-5
  (member-type-5 (genera-facet-5-simplex simplex)))

(defthm genera-facet-6-simplex-member-type-6
  (member-type-6 (genera-facet-6-simplex simplex)))



;;;---------------------------------------------------------------------------
;;;
;;; Auxiliary lemmas
;;;
;;;---------------------------------------------------------------------------

(defthm list-0-1-not
  (implies (not (list-0-1p (cdr x)))
	   (not (list-0-1p x))))

(defthm list-of-lists-of-0-1-not
  (implies (not (list-of-lists-of-0-1p (cdr x)))
	   (not (list-of-lists-of-0-1p x))))

(defthm 3d-imagep-not
  (implies (not (3d-imagep (cdr image)))
	   (not (3d-imagep image))))

(defthm member-equal-append
  (implies (member-equal a b)
	   (member-equal a (append c b))))

(defthm append-member-not
  (implies (and (not (member-equal a c))
		(member-equal a (append b c)))
	   (member-equal a b)))

(defthm member-equal-append-2
  (implies (member-equal a b)
	   (member-equal a (append b c))))


;;;---------------------------------------------------------------------------
;;;
;;; Verification of the correctness of the algorithm genera-facets-image-3d
;;;
;;;---------------------------------------------------------------------------


;;;***************************************************************************
;;;
;;; If one of the simplexes is in the generated list, all its partners too
;;;
;;;***************************************************************************


(defthm member-equal-genera-facets-3d-image-aux
  (implies (and (consp image)
		(member-equal a (genera-facets-3d-image-aux (cdr image) (1+ j))))
	   (member-equal a (genera-facets-3d-image-aux image j))))


(encapsulate

()

(local (defthm member-equal-genera-facets-line-1-2
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-1 simplex))
	   (member-equal (genera-facet-2-simplex simplex) 
			 (genera-facets-line x i j k)))))

(local (defthm member-equal-genera-facets-line-2-3
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-2 simplex))
	   (member-equal (genera-facet-3-simplex simplex) 
			 (genera-facets-line x i j k)))))

(local (defthm member-equal-genera-facets-line-3-4
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-3 simplex))
	   (member-equal (genera-facet-4-simplex simplex) 
			 (genera-facets-line x i j k)))))

(local (defthm member-equal-genera-facets-line-4-5
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-4 simplex))
	   (member-equal (genera-facet-5-simplex simplex) 
			 (genera-facets-line x i j k)))))

(local (defthm member-equal-genera-facets-line-5-6
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-5 simplex))
	   (member-equal (genera-facet-6-simplex simplex) 
			 (genera-facets-line x i j k)))))

(local (defthm member-equal-genera-facets-line-6-1
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-6 simplex))
	   (member-equal (genera-facet-1-simplex simplex) 
			 (genera-facets-line x i j k)))))


(local (defthm member-equal-genera-facets-line-1
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-1 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-3-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-4-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-5-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-6-simplex simplex) 
			      (genera-facets-line x i j k))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-line-1-2)
		 (:instance genera-facet-2-simplex-member-type-2)
		 (:instance member-equal-genera-facets-line-2-3 
			    (simplex (genera-facet-2-simplex simplex)))
		 (:instance genera-facet-3-simplex-member-type-3)
		 (:instance member-equal-genera-facets-line-3-4 
			    (simplex (genera-facet-3-simplex (genera-facet-2-simplex simplex))))
		 (:instance genera-facet-4-simplex-member-type-4)
		 (:instance member-equal-genera-facets-line-4-5 
			    (simplex (genera-facet-4-simplex (genera-facet-3-simplex (genera-facet-2-simplex simplex)))))
		 (:instance genera-facet-5-simplex-member-type-5)
		 (:instance member-equal-genera-facets-line-5-6 
			    (simplex (genera-facet-5-simplex (genera-facet-4-simplex (genera-facet-3-simplex (genera-facet-2-simplex simplex)))))
		 ))))))


(local (defthm member-equal-genera-facets-line-2
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-2 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-3-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-4-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-5-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-6-simplex simplex) 
			      (genera-facets-line x i j k))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-line-2-3)
		 (:instance genera-facet-3-simplex-member-type-3)
		 (:instance member-equal-genera-facets-line-3-4 
			    (simplex (genera-facet-3-simplex simplex)))
		 (:instance genera-facet-4-simplex-member-type-4)
		 (:instance member-equal-genera-facets-line-4-5 
			    (simplex (genera-facet-4-simplex (genera-facet-3-simplex simplex))))
		 (:instance genera-facet-5-simplex-member-type-5)
		 (:instance member-equal-genera-facets-line-5-6 
			    (simplex (genera-facet-5-simplex (genera-facet-4-simplex (genera-facet-3-simplex simplex)))))
		 (:instance genera-facet-6-simplex-member-type-6)
		 (:instance member-equal-genera-facets-line-6-1 
			    (simplex (genera-facet-6-simplex (genera-facet-5-simplex (genera-facet-4-simplex (genera-facet-3-simplex simplex)))))
		 ))))))


(local (defthm member-equal-genera-facets-line-3
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-3 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-2-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-4-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-5-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-6-simplex simplex) 
			      (genera-facets-line x i j k))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-line-3-4)
		 (:instance genera-facet-4-simplex-member-type-4)
		 (:instance member-equal-genera-facets-line-4-5 
			    (simplex (genera-facet-4-simplex simplex)))
		 (:instance genera-facet-5-simplex-member-type-5)
		 (:instance member-equal-genera-facets-line-5-6 
			    (simplex (genera-facet-5-simplex (genera-facet-4-simplex simplex))))
		 (:instance genera-facet-6-simplex-member-type-6)
		 (:instance member-equal-genera-facets-line-6-1 
			    (simplex (genera-facet-6-simplex (genera-facet-5-simplex (genera-facet-4-simplex simplex)))))
		 (:instance genera-facet-1-simplex-member-type-1)
		 (:instance member-equal-genera-facets-line-1-2 
			    (simplex (genera-facet-1-simplex (genera-facet-6-simplex (genera-facet-5-simplex (genera-facet-4-simplex simplex)))))
		 ))))))


(local (defthm member-equal-genera-facets-line-4
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-4 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-2-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-3-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-5-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-6-simplex simplex) 
			      (genera-facets-line x i j k))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-line-4-5)
		 (:instance genera-facet-5-simplex-member-type-5)
		 (:instance member-equal-genera-facets-line-5-6 
			    (simplex (genera-facet-5-simplex simplex)))
		 (:instance genera-facet-6-simplex-member-type-6)
		 (:instance member-equal-genera-facets-line-6-1 
			    (simplex (genera-facet-6-simplex (genera-facet-5-simplex simplex))))
		 (:instance genera-facet-1-simplex-member-type-1)
		 (:instance member-equal-genera-facets-line-1-2 
			    (simplex (genera-facet-1-simplex (genera-facet-6-simplex (genera-facet-5-simplex simplex)))))
		 (:instance genera-facet-2-simplex-member-type-2)
		 (:instance member-equal-genera-facets-line-2-3 
			    (simplex (genera-facet-2-simplex (genera-facet-1-simplex (genera-facet-6-simplex (genera-facet-5-simplex simplex)))))
		 ))))))


(local (defthm member-equal-genera-facets-line-5
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-5 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-2-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-3-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-4-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-6-simplex simplex) 
			      (genera-facets-line x i j k))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-line-5-6)
		 (:instance genera-facet-6-simplex-member-type-6)
		 (:instance member-equal-genera-facets-line-6-1 
			    (simplex (genera-facet-6-simplex simplex)))
		 (:instance genera-facet-1-simplex-member-type-1)
		 (:instance member-equal-genera-facets-line-1-2 
			    (simplex (genera-facet-1-simplex (genera-facet-6-simplex simplex))))
		 (:instance genera-facet-2-simplex-member-type-2)
		 (:instance member-equal-genera-facets-line-2-3 
			    (simplex (genera-facet-2-simplex (genera-facet-1-simplex (genera-facet-6-simplex simplex)))))
		 (:instance genera-facet-3-simplex-member-type-3)
		 (:instance member-equal-genera-facets-line-3-4 
			    (simplex (genera-facet-3-simplex (genera-facet-2-simplex (genera-facet-1-simplex (genera-facet-6-simplex simplex)))))
		 ))))))

(local (defthm member-equal-genera-facets-line-6
  (implies (and (member-equal simplex (genera-facets-line x i j k))
		(member-type-6 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-2-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-3-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-4-simplex simplex) 
			      (genera-facets-line x i j k))
		(member-equal (genera-facet-5-simplex simplex) 
			      (genera-facets-line x i j k))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-line-6-1)
		 (:instance genera-facet-1-simplex-member-type-1)
		 (:instance member-equal-genera-facets-line-1-2 
			    (simplex (genera-facet-1-simplex simplex)))
		 (:instance genera-facet-2-simplex-member-type-2)
		 (:instance member-equal-genera-facets-line-2-3 
			    (simplex (genera-facet-2-simplex (genera-facet-1-simplex simplex))))
		 (:instance genera-facet-3-simplex-member-type-3)
		 (:instance member-equal-genera-facets-line-3-4 
			    (simplex (genera-facet-3-simplex (genera-facet-2-simplex (genera-facet-1-simplex simplex)))))
		 (:instance genera-facet-4-simplex-member-type-4)
		 (:instance member-equal-genera-facets-line-4-5 
			    (simplex (genera-facet-4-simplex (genera-facet-3-simplex (genera-facet-2-simplex (genera-facet-1-simplex simplex)))))
		 ))))))



(local (defthm member-equal-genera-facets-layer-1
  (implies (and (member-equal simplex (genera-facets-layer x j k))
		(member-type-1 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-layer x j k))))
  :hints (("Goal" :in-theory (disable member-type-1 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-layer-2
  (implies (and (member-equal simplex (genera-facets-layer x j k))
		(member-type-2 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-layer x j k))))
  :hints (("Goal" :in-theory (disable member-type-2 genera-facet-1-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-layer-3
  (implies (and (member-equal simplex (genera-facets-layer x j k))
		(member-type-3 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-layer x j k))))
  :hints (("Goal" :in-theory (disable member-type-3 genera-facet-2-simplex
				      genera-facet-1-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-layer-4
  (implies (and (member-equal simplex (genera-facets-layer x j k))
		(member-type-4 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-layer x j k))))
  :hints (("Goal" :in-theory (disable member-type-4 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-1-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-layer-5
  (implies (and (member-equal simplex (genera-facets-layer x j k))
		(member-type-5 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-layer x j k))))
  :hints (("Goal" :in-theory (disable member-type-5 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-1-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-layer-6
  (implies (and (member-equal simplex (genera-facets-layer x j k))
		(member-type-6 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-layer x j k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-layer x j k))))
  :hints (("Goal" :in-theory (disable member-type-6 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-1-simplex)))))



(local (defthm member-equal-genera-facets-3d-image-aux-1
  (implies (and (member-equal simplex (genera-facets-3d-image-aux x k))
		(member-type-1 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-3d-image-aux x k))))
  :hints (("Goal" :in-theory (disable member-type-1 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-3d-image-aux-2
  (implies (and (member-equal simplex (genera-facets-3d-image-aux x k))
		(member-type-2 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-3d-image-aux x k))))
  :hints (("Goal" :in-theory (disable member-type-2 genera-facet-1-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))


(local (defthm member-equal-genera-facets-3d-image-aux-3
  (implies (and (member-equal simplex (genera-facets-3d-image-aux x k))
		(member-type-3 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-3d-image-aux x k))))
  :hints (("Goal" :in-theory (disable member-type-3 genera-facet-2-simplex
				      genera-facet-1-simplex
				      genera-facet-4-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-3d-image-aux-4
  (implies (and (member-equal simplex (genera-facets-3d-image-aux x k))
		(member-type-4 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-3d-image-aux x k))))
  :hints (("Goal" :in-theory (disable member-type-4 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-1-simplex
				      genera-facet-5-simplex
				      genera-facet-6-simplex)))))

(local (defthm member-equal-genera-facets-3d-image-aux-5
  (implies (and (member-equal simplex (genera-facets-3d-image-aux x k))
		(member-type-5 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-3d-image-aux x k))))
  :hints (("Goal" :in-theory (disable member-type-5 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-1-simplex
				      genera-facet-6-simplex)))))


(local (defthm member-equal-genera-facets-3d-image-aux-6
  (implies (and (member-equal simplex (genera-facets-3d-image-aux x k))
		(member-type-6 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-3d-image-aux x k))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-3d-image-aux x k))))
  :hints (("Goal" :in-theory (disable member-type-6 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-1-simplex
				      genera-facet-5-simplex)))))



(defthm member-equal-genera-facets-image-3d-1
  (implies (and (member-equal simplex (genera-facets-image-3d x))
		(member-type-1 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-image-3d x))))
  :hints (("Goal" :in-theory (disable member-type-1 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-6-simplex
				      genera-facet-5-simplex))))

(defthm member-equal-genera-facets-image-3d-2
  (implies (and (member-equal simplex (genera-facets-image-3d x))
		(member-type-2 simplex))
	   (and (member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-image-3d x))))
  :hints (("Goal" :in-theory (disable member-type-2 genera-facet-1-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-6-simplex
				      genera-facet-5-simplex))))

(defthm member-equal-genera-facets-image-3d-3
  (implies (and (member-equal simplex (genera-facets-image-3d x))
		(member-type-3 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-image-3d x))))
  :hints (("Goal" :in-theory (disable member-type-3 genera-facet-2-simplex
				      genera-facet-1-simplex
				      genera-facet-4-simplex
				      genera-facet-6-simplex
				      genera-facet-5-simplex))))

(defthm member-equal-genera-facets-image-3d-4
  (implies (and (member-equal simplex (genera-facets-image-3d x))
		(member-type-4 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-image-3d x))))
  :hints (("Goal" :in-theory (disable member-type-4 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-1-simplex
				      genera-facet-6-simplex
				      genera-facet-5-simplex))))

(defthm member-equal-genera-facets-image-3d-5
  (implies (and (member-equal simplex (genera-facets-image-3d x))
		(member-type-5 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-6-simplex simplex)
			      (genera-facets-image-3d x))))
  :hints (("Goal" :in-theory (disable member-type-5 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-6-simplex
				      genera-facet-1-simplex))))

(defthm member-equal-genera-facets-image-3d-6
  (implies (and (member-equal simplex (genera-facets-image-3d x))
		(member-type-6 simplex))
	   (and (member-equal (genera-facet-2-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-3-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-4-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-5-simplex simplex)
			      (genera-facets-image-3d x))
		(member-equal (genera-facet-1-simplex simplex)
			      (genera-facets-image-3d x))))
  :hints (("Goal" :in-theory (disable member-type-6 genera-facet-2-simplex
				      genera-facet-3-simplex
				      genera-facet-4-simplex
				      genera-facet-1-simplex
				      genera-facet-5-simplex))))

)

;;;***************************************************************************
;;;
;;; If a simplex ((i,j,k),(),(),()) is in genera-facets-image-3d image
;;; that means that the element of position (i,j,k) of image is a 1
;;;
;;;***************************************************************************

(encapsulate
 ()

   
(local (defthm natp-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (natp (nth 0 (car simplex))))))


(local(defthm nth-0>=k-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (<= i (nth 0 (car simplex))))))

(local(defthm nth-0<len-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (<  (nth 0 (car simplex)) (+ (len x) i)))))


(local(defthm natp-member-equal-genera-facets-line-caar
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (natp (caar simplex)))))


(local (defthm caar>=k-member-equal-genera-facets-list
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (<= i (caar simplex)))))

(local (defthm caar<len-member-equal-genera-facets-list
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (< (caar simplex) (+ (len x) i)))))
		

(local (defthm member-genera-facets-line-cdr
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line (cdr x) (1+ i) j k)))
	   (member-equal simplex (genera-facets-line x i j k))))
)

(defthm nth-cdr
  (implies (and (natp i)
		(> i 0))
	   (equal (nth (- i 1) (cdr x))
		  (nth i x))))


(defthm auxiliar-1
  (implies (and (natp i)
		(natp j)
		(< i j))
	   (equal (+ (- (+ 1 i)) j)
		  (- (- j i) 1)))
  :rule-classes nil)

(defthm auxiliar-2
  (implies (and (natp i)
		(natp j)
		(< i j))
	   (equal (+ (- i) j)
		  (- j i)))
  :rule-classes nil)


(defthm auxiliar-3
  (implies (and (natp i)
		(natp j)
		(< i j))
	   (equal (nth (+ (- (+ 1 i)) j) (cdr x))
		  (nth (+ (- i) j) x)))
  :hints (("Goal"  :use ((:instance auxiliar-1)
			 (:instance auxiliar-2)
			 (:instance nth-cdr (i (- j i)))))))

(defthm transitive
  (implies (and (natp x)
		(natp y)
		(<= (1+ x) y))
	   (< x y)))


(local (defthm nth-0>k-member-equal-genera-facets-line-cdr
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x (1+ i) j k)))
	   (< i (nth 0 (car simplex))))
  :hints (("Goal" :use ((:instance natp-member-equal-genera-facets-line
				   (i (1+ i)))
			(:instance nth-0>=k-member-equal-genera-facets-line
				  (i (1+ i)))
			(:instance transitive (x i) (y (nth 0 (car simplex))))))))
       )

(local (defthm facets-line-well-defined-aux-1
  (implies (and (list-0-1p (cdr x))
		(equal (car x) 0)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth (+ (nth 0 (car simplex)) (- (+ 1 i))) (cdr x)) 1)
		(member-equal simplex (genera-facets-line (cdr x) (1+ i) j k)))
	   (equal (nth (+ (nth 0 (car simplex)) (- i)) x) 1))
    :hints (("Goal" 
	   :use ((:instance natp-member-equal-genera-facets-line (x (cdr x)) (i (1+ i)))
		 (:instance nth-0>=k-member-equal-genera-facets-line (x (cdr x)) (i (1+ i)))
		 (:instance nth-0>k-member-equal-genera-facets-line-cdr)))
	  )))

(local (defthm facets-line-well-defined-aux-2
  (implies (and (list-0-1p (cdr x))
		(equal (car x) 1)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth (+ (nth 0 (car simplex)) (- (+ 1 i))) (cdr x)) 1)
		(member-equal simplex (genera-facets-line (cdr x) (1+ i) j k)))
	   (equal (nth (+ (nth 0 (car simplex)) (- i)) x) 1))
    :hints (("Goal" 
	   :use ((:instance natp-member-equal-genera-facets-line (x (cdr x)) (i (1+ i)))
		 (:instance nth-0>=k-member-equal-genera-facets-line (x (cdr x)) (i (1+ i)))
		 (:instance nth-0>k-member-equal-genera-facets-line-cdr)))
	  )))


(defthm nth-0-caar 
  (equal (nth 0 (car x))
	 (caar x)))


(defthm equal-nths
  (implies (and (consp y)
		(natp i)
		(< 0 i))
	   (equal (nth (- i 1) (cdr y))
		  (nth i y))))


(local (defthm facets-line-well-defined-help-2
  (IMPLIES (AND (NOT (ENDP X))
              (NOT (EQUAL (CAR X) 1))
              (IMPLIES (AND (LIST-0-1P (CDR X))
                            (NATP (+ 1 I))
                            (NATP J)
                            (NATP K)
                            (MEMBER-EQUAL SIMPLEX
                                          (GENERA-FACETS-LINE (CDR X)
                                                              (+ 1 I)
                                                              J K)))
                       (EQUAL (NTH (+ (NTH 0 (CAR SIMPLEX)) (- (+ 1 I)))
                                   (CDR X))
                              1)))
         (IMPLIES (AND (LIST-0-1P X)
                       (NATP I)
                       (NATP J)
                       (NATP K)
                       (MEMBER-EQUAL SIMPLEX (GENERA-FACETS-LINE X I J K)))
                  (EQUAL (NTH (+ (NTH 0 (CAR SIMPLEX)) (- I)) X)
                         1)))))


(local (defthm facets-line-well-defined-help
  (IMPLIES (AND (NOT (ENDP X))
              (EQUAL (CAR X) 1)
              (IMPLIES (AND (LIST-0-1P (CDR X))
                            (NATP (+ 1 I))
                            (NATP J)
                            (NATP K)
                            (MEMBER-EQUAL SIMPLEX
                                          (GENERA-FACETS-LINE (CDR X)
                                                              (+ 1 I)
                                                              J K)))
                       (EQUAL (NTH (+ (NTH 0 (CAR SIMPLEX)) (- (+ 1 I)))
                                   (CDR X))
                              1)))
         (IMPLIES (AND (LIST-0-1P X)
                       (NATP I)
                       (NATP J)
                       (NATP K)
                       (MEMBER-EQUAL SIMPLEX (GENERA-FACETS-LINE X I J K)))
                  (EQUAL (NTH (+ (NTH 0 (CAR SIMPLEX)) (- I)) X)
                         1)))))
   
(local (defthm facets-line-well-defined
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (equal (nth (+ (nth 0 (car simplex)) (- i)) x) 1))
  :hints (("Subgoal *1/3" :use (:instance facets-line-well-defined-help-2))
	  ("Subgoal *1/2" :use (:instance facets-line-well-defined-help))))
 )


(local (defthm natp-nth-1-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (natp (nth 1 (car simplex))))))

(local (defthm natp-cadar-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (natp (cadar simplex)))))

(local (defthm nth-1>=j-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (<= j (nth 1 (car simplex))))))

(local (defthm cadar>=k-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (<= j (cadar simplex)))))


(local (defthm natp-nth-1-member-equal-genera-facets-layer
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (natp (nth 1 (car simplex))))
  :hints (("Subgoal *1/2" :use
	   (:instance natp-nth-1-member-equal-genera-facets-line
		      (x (car x))
		      (i 0))))))

(local (defthm nth-1>=k-member-equal-genera-facets-image-aux
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (<= j (nth 1 (car simplex))))
  :hints (("Subgoal *1/2" :use
	   (:instance nth-1>=j-member-equal-genera-facets-line
		      (x (car x))
		      (i 0))))))

(local (defthm nth-1=k-member-equal-genera-facets-list
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (equal (nth 1 (car simplex)) j))))


(local (defthm well-defined-genera-facets-layer-aux
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (equal (nth (+ (- j) (nth 1 (car simplex))) y)
		  (car y)))))



(local (defthm well-defined-genera-facets-layer-aux-1
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(not (member-equal simplex (genera-facets-layer
					    (cdr x) (1+ j) k)))
		(member-equal simplex (append (genera-facets-line (car x)
								  0 j k)
					     (genera-facets-layer
					    (cdr x) (1+ j) k) ))
		)
	   (equal (nth (nth 0 (car simplex))
		       (nth (+ (nth 1 (car simplex)) (- j))
			    x)) 1))
  :hints (("Goal" :use 
	   ((:instance  append-member-not
			(a simplex)
			(c (genera-facets-layer (cdr x) (1+ j) k))
			(b (genera-facets-line (car x) 0 j k)))
	    (:instance well-defined-genera-facets-layer-aux
		       (x (car x))
		       (y x)
		       (i 0))
	    (:instance facets-line-well-defined
		       (x (car x))
		       (i 0)))))))

(local (defthm well-defined-genera-facets-layer-aux-2
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(not (member-equal simplex (genera-facets-layer
					    (cdr x) (1+ j) k)))
		(member-equal simplex (append (genera-facets-line (car x)
								  0 j k)
					     (genera-facets-layer
					    (cdr x) (1+ j) k) ))
		)
	   (equal (nth (caar simplex)
		       (nth (+ (nth 1 (car simplex)) (- j))
			    x)) 1))
  :hints (("Goal" :use 
	   ((:instance  append-member-not
			(a simplex)
			(c (genera-facets-layer (cdr x) (1+ j) k))
			(b (genera-facets-line (car x) 0 j k)))
	    (:instance well-defined-genera-facets-layer-aux
		       (x (car x))
		       (y x)
		       (i 0))
	    (:instance facets-line-well-defined
		       (x (car x))
		       (i 0)))))))


(local (defthm well-defined-genera-facets-layer-aux-3
  (IMPLIES (AND (NOT (ENDP X))
		(IMPLIES (AND (LIST-OF-LISTS-OF-0-1P (CDR X))
			      (NATP (+ 1 J))
			      (NATP K)
			      (MEMBER-EQUAL SIMPLEX
					    (GENERA-FACETS-LAYER (CDR X)
								 (+ 1 J)
                                                               K)))
			 (EQUAL (NTH (NTH 0 (CAR SIMPLEX))
				     (NTH (+ (NTH 1 (CAR SIMPLEX)) (- (+ 1 J)))
					  (CDR X)))
				1)))
	   (IMPLIES (AND (LIST-OF-LISTS-OF-0-1P X)
			 (NATP J)
			 (NATP K)
			 (MEMBER-EQUAL SIMPLEX (GENERA-FACETS-LAYER X J K)))
		    (EQUAL (NTH (NTH 0 (CAR SIMPLEX))
				(NTH (+ (NTH 1 (CAR SIMPLEX)) (- J)) X))
			   1)))
  :hints (("Goal" :do-not-induct t
	   :use (:instance well-defined-genera-facets-layer-aux-2)))))



(local (defthm well-defined-genera-facets-layer
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (equal (nth (nth 0 (car simplex))
		       (nth (+ (nth 1 (car simplex)) (- j))
			    x)) 1))
  :hints (("Subgoal *1/2" :use 
	   ((:instance well-defined-genera-facets-layer-aux-3)
	    )))))


(local (defthm nth-2=k-member-equal-genera-facets-list
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (equal (nth 2 (car simplex)) k))))


(local (defthm nth-2=k-member-equal-genera-facets-layer
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (equal (nth 2 (car simplex)) k))
  :hints (("Subgoal *1/2''"
	   :use ((:instance  append-member-not
			(a simplex)
			(c (genera-facets-layer (cdr x) (1+ j) k))
			(b (genera-facets-line (car x) 0 j k)))
		 (:instance nth-2=k-member-equal-genera-facets-list
			    (x (car x))
			    (i 0)))))))



(local (defthm nth-2->=k-member-equal-genera-facets-layer-aux
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (<= k (nth 2 (car simplex))))))

(local (defthm nth-2->=k-member-equal-genera-facets-3d-image-aux
  (implies (and (3d-imagep x)
		(natp k)
		(member-equal simplex (genera-facets-3d-image-aux x k)))
	   (<= k (nth 2 (car simplex))))
  :hints (("Subgoal *1/2''"
	   :use ((:instance  append-member-not
			(a simplex)
			(c (genera-facets-3d-image-aux (cdr x) (1+ k)))
			(b (genera-facets-layer (car x) 0 k)))
		 (:instance nth-2->=k-member-equal-genera-facets-layer-aux
			    (x (car x))
			    (j 0)))))))


(local (defthm natp-nth-2-member-equal-genera-facets-line
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-line x i j k)))
	   (natp (nth 2 (car simplex))))))


(local (defthm natp-nth-2-member-equal-genera-facets-layer
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (natp (nth 2 (car simplex))))))

(local (defthm natp-nth-2-member-equal-genera-facets-3d-image-aux
  (implies (and (3d-imagep x)
		(natp k)
		(member-equal simplex (genera-facets-3d-image-aux x k)))
	   (natp (nth 2 (car simplex))))
  :hints (("Subgoal *1/2"
	   :use ((:instance  append-member-not
			(a simplex)
			(c (genera-facets-3d-image-aux (cdr x) (1+ k)))
			(b (genera-facets-layer (car x) 0 k)))
		 (:instance natp-nth-2-member-equal-genera-facets-layer
			    (x (car x))
			    (j 0)))))))

(local (defthm nth-2->=k-member-equal-genera-facets-3d-image-aux-2
  (implies (and (3d-imagep x)
		(natp k)
		(member-equal simplex (genera-facets-3d-image-aux x (1+ k))))
	   (< k (nth 2 (car simplex))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance natp-nth-2-member-equal-genera-facets-3d-image-aux
			    (k (1+ k)))
		 (:instance nth-2->=k-member-equal-genera-facets-3d-image-aux
			    	    (k (1+ k)))
		 (:instance transitive (x k) (y (nth 2 (car simplex))))))))
       )



(local (defthm well-defined-genera-facets-3d-aux
  (implies (and (list-of-lists-of-0-1p x)
		(natp j)
		(natp k)
		(member-equal simplex (genera-facets-layer x j k)))
	   (equal (nth (+ (- k) (nth 2 (car simplex))) y)
		  (car y)))))

(local 
(defthm well-defined-genera-facets-3d-image-aux-help-1
  (IMPLIES (AND (CONSP image)
		(NOT (MEMBER-EQUAL SIMPLEX
				   (GENERA-FACETS-3D-IMAGE-AUX (CDR image)
							       (+ 1 K))))
		(|3D-IMAGEP| IMAGE)
		(INTEGERP K)
		(<= 0 K)
		(MEMBER-EQUAL SIMPLEX
			      (APPEND (GENERA-FACETS-LAYER (CAR image) 0 K)
				      (GENERA-FACETS-3D-IMAGE-AUX (CDR image)
								  (+ 1 K)))))
	   (EQUAL (NTH (CAAR SIMPLEX)
		       (NTH (NTH 1 (CAR SIMPLEX))
			    (NTH (+ (- K) (NTH 2 (CAR SIMPLEX)))
				 IMAGE)))
		  1))
  :hints (("Goal" :use 
	   ((:instance append-member-not
			(a simplex)
			(c (genera-facets-3d-image-aux (cdr image) (1+ k)))
			(b (genera-facets-layer (car image) 0 k)))
	    (:instance well-defined-genera-facets-3d-aux
		       (x (car image))
		       (y image)
		       (j 0))
	    (:instance  well-defined-genera-facets-layer
		       (x (car image))
		       (j 0)))))
  ))


(local 
(defthm well-defined-genera-facets-3d-image-aux-help-2
  (IMPLIES (AND (3D-IMAGEP IMAGE)
		(natp k)
		(MEMBER-EQUAL SIMPLEX (GENERA-FACETS-LAYER (CAR image) 0 K)))
	   (EQUAL (NTH (CAAR SIMPLEX)
		       (NTH (NTH 1 (CAR SIMPLEX))
			    (NTH (+ (- K) (NTH 2 (CAR SIMPLEX)))
				 IMAGE)))
		  1))
  :hints (("Goal" :use 
	   ((:instance well-defined-genera-facets-3d-aux
		       (x (car image))
		       (y image)
		       (j 0))
	    (:instance  well-defined-genera-facets-layer
		       (x (car image))
		       (j 0)))))
  ))

(local 
(defthm well-defined-genera-facets-3d-image-aux-help-3
  (IMPLIES
    (AND (NOT (ENDP IMAGE))
         (IMPLIES (AND (|3D-IMAGEP| (CDR IMAGE))
                       (NATP (+ 1 K))
                       (MEMBER-EQUAL SIMPLEX
                                     (GENERA-FACETS-3D-IMAGE-AUX (CDR IMAGE)
                                                                 (+ 1 K))))
                  (EQUAL (NTH (NTH 0 (CAR SIMPLEX))
                              (NTH (NTH 1 (CAR SIMPLEX))
                                   (NTH (+ (NTH 2 (CAR SIMPLEX)) (- (+ 1 K)))
                                        (CDR IMAGE))))
                         1)))
    (IMPLIES (AND (|3D-IMAGEP| IMAGE)
                  (NATP K)
                  (MEMBER-EQUAL SIMPLEX
                                (GENERA-FACETS-3D-IMAGE-AUX IMAGE K)))
             (EQUAL (NTH (NTH 0 (CAR SIMPLEX))
                         (NTH (NTH 1 (CAR SIMPLEX))
                              (NTH (+ (NTH 2 (CAR SIMPLEX)) (- K))
                                   IMAGE)))
                    1)))))

(local 
(defthm well-defined-genera-facets-3d-image-aux
  (implies (and (3d-imagep image)
		(natp k)
		(member-equal simplex (genera-facets-3d-image-aux image k)))
	   (equal (nth (nth 0 (car simplex))
		       (nth (nth 1 (car simplex))
			    (nth (+ (nth 2 (car simplex)) (- k)) image)))
		  1))
  :hints (("Subgoal *1/2" :use
	   (:instance well-defined-genera-facets-3d-image-aux-help-3))))
		)


(defthm well-defined-genera-facets-image-3d
  (implies (and (3d-imagep image)		
		(member-equal simplex (genera-facets-image-3d image)))
	   (equal
	    (nth (nth 0 (car simplex))
		 (nth (nth 1 (car simplex))
		      (nth (nth 2 (car simplex)) image)))
	    1))
  :hints (("Subgoal *1/2" :use
	   (:instance well-defined-genera-facets-3d-image-aux (k 0)))))


)


;;;---------------------------------------------------------------------------
;;;
;;; Verification of the completeness of the algorithm genera-facets-image-3d
;;;
;;;---------------------------------------------------------------------------

(encapsulate
 ()

(local (defthm --1-i-1-l
  (implies (and (natp i)
		(natp l))
	   (equal (+ -1 i 1 l)
		  (+ i l)))))

(local (defthm member-equal-genera-facets-line-nth
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(natp l)
		(equal (nth i x) 1))
	   (member-equal (genera-facet-1 (+ i l) j k) (genera-facets-line x l j k))
  )))


(local (defthm member-equal-genera-facets-line-nth-case-0
  (implies (and (list-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth i x) 1))
	   (member-equal (genera-facet-1 i j k) (genera-facets-line x 0 j k))
  )
  :hints (("Goal" :use ((:instance member-equal-genera-facets-line-nth (l 0)))))))

(local (defthm genera-facets-layer-completeness
  (implies (and (list-of-lists-of-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(natp l)
		(equal (nth i (nth j x)) 1))
	   (member-equal (genera-facet-1 i (+ j l) k) (genera-facets-layer x l k))
  )
:hints (("Goal" :in-theory (disable genera-facet-1)))))


(local (defthm genera-facets-layer-completeness-case
  (implies (and (list-of-lists-of-0-1p x)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth i (nth j x)) 1))
	   (member-equal (genera-facet-1 i j k) (genera-facets-layer x 0 k))
  )
:hints (("Goal" :in-theory (disable genera-facet-1)
	 :use ((:instance genera-facets-layer-completeness (l 0)))))))


(local (defthm genera-facets-3d-image-aux-completeness
  (implies (and (3d-imagep x)
		(natp i)
		(natp j)
		(natp k)
		(natp l)
		(equal (nth i (nth j (nth k x))) 1))
	   (member-equal (genera-facet-1 i j (+ k l)) (genera-facets-3d-image-aux x l))
  )
:hints (("Goal" :in-theory (disable genera-facet-1)))))

(local (defthm genera-facets-3d-image-aux-completeness-case
  (implies (and (3d-imagep x)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth i (nth j (nth k x))) 1))
	   (member-equal (genera-facet-1 i j k) (genera-facets-3d-image-aux x 0))
  )
  :hints (("Goal" :in-theory (disable genera-facet-1)
	 :use ((:instance genera-facets-3d-image-aux-completeness (l 0))))))
       )

(local (defthm genera-facets-image-3d-completeness-1
  (implies (and (3d-imagep image)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth i (nth j (nth k image))) 1))
	   (member-equal (genera-facet-1 i j k) (genera-facets-image-3d image))
  )
  :hints (("Goal" :in-theory (disable genera-facet-1)
	   :use (:instance  genera-facets-3d-image-aux-completeness-case
			   (k 0))))))


(local (defthm equality-genera-facet-1-2
  (equal (genera-facet-2 i j k)
	 (genera-facet-2-simplex (genera-facet-1 i j k)))))

(local (defthm equality-genera-facet-1-3
  (equal (genera-facet-3 i j k)
	 (genera-facet-3-simplex (genera-facet-1 i j k)))))

(local (defthm equality-genera-facet-1-4
  (equal (genera-facet-4 i j k)
	 (genera-facet-4-simplex (genera-facet-1 i j k)))))

(local (defthm equality-genera-facet-1-5
  (equal (genera-facet-5 i j k)
	 (genera-facet-5-simplex (genera-facet-1 i j k)))))

(local (defthm equality-genera-facet-1-6
  (equal (genera-facet-6 i j k)
	 (genera-facet-6-simplex (genera-facet-1 i j k)))))



(defthm genera-facets-image-3d-completeness
  (implies (and (3d-imagep image)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth i (nth j (nth k image))) 1))
	   (and (member-equal (genera-facet-1 i j k) (genera-facets-image-3d image))
		(member-equal (genera-facet-2 i j k) (genera-facets-image-3d image))
		(member-equal (genera-facet-3 i j k) (genera-facets-image-3d image))
		(member-equal (genera-facet-4 i j k) (genera-facets-image-3d image))
		(member-equal (genera-facet-5 i j k) (genera-facets-image-3d image))
		(member-equal (genera-facet-6 i j k) (genera-facets-image-3d image))
		))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance member-equal-genera-facets-image-3d-1
			    (x image)
			    (simplex (genera-facet-1 i j k)))
		 (:instance genera-facets-image-3d-completeness-1)
		 ))))
  


)